$\forall$${\it es}$:ES, $T$:Type, $l$:IdLnk, ${\it tg}$, $a$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$($T$ + Top)).
\\[0ex]weak{-}send{-}do{-}apply(${\it es}$;$T$;$l$;${\it tg}$;$a$;${\it ds}$;$f$) $\in$ $\mathbb{P}$